es:ES, A:Type, X, Y:AbsInterface(A), e:E.
((e  [X?Y]))  ([X?Y](e) = if e  X then X(e) else Y(e) fi   A) 

latex

Definitions	x:A. B(x), isl(x), t  T, b, P  Q, outl(x), True, x:AB(x), do-apply(f;x), can-apply(f;x), X(e), e  X, [f?g], AbsInterface(A), E, Type, ES, f(a), Top, left + right, s = t
Lemmas	true wf, outl wf, assert wf, isl wf